w:World, a, b:E. FairFifo  (w_locle(w;a;b)  (loc(a) = loc(b)  Id & (a < b  (a = b)))) 

latex

Definitions	t  T, x:A. B(x), FairFifo, x:AB(x), Id, w-info(w;e), e < e', left + right, x:A  B(x), P & Q, P  Q, World, E, s = t, w_locl(w;x;y), P  Q, w_locle(w;x;y), P  Q, x:A. B(x), , w-pred(w;e), x.A(x), pred(e), first(e), b, A, Type, A c B, rel_exp(T;R;n), f(a), , , Void, False, P  Q, x f y, R^+, R^*, {T}, SQType(T), , s ~ t, A  B, {x:A| B(x)} , #$n, Dec(P), <a, b>, (i = j), a < b, loc(e), True, T, IdLnk
Lemmas	squash wf, true wf, IdLnk wf, w locle wf, iff functionality wrt iff, or functionality wrt iff, w locl-lemma, w locl wf, loc wf, cless wf, Id wf, w-info wf, le wf, decidable int equal, nat wf, nat plus wf, rel exp wf, nat plus inc, not wf, assert wf, first wf, pred wf, w-pred wf, world wf, w-E wf, fair-fifo wf